COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "let.pub[let,jmc]" source
C00006 ENDMK
C⊗;
.require "let.pub[let,jmc]" source;
∂CSL Professor W. W. Bledsoe↓Department of Mathematics
↓University of Texas↓Austin, Texas 78712∞

Dear Woody:

	I hope to make the meeting in SF, possibly a bit late
because of a class.  Anyway I have an idea for an intermediate
prize.

	The program used to verify the four-color theorem was never
proved correct - either by hand or machine.  It is disgraceful that
the referees wrote their own program.  It is almost as though a
proof was offered that consisted of a selection of cases and the
referees accepted the paper on the basis of some further examples.

	Whether one regards the above analogy as valid or not, it
is clear that assurance of the correctness of the four color conjecture
would be greater if the program had been proved to meet certain
specifications.  Even suppose that no-one had proved anything aobut
the programming language, the compiler or the computer itself.
It is ultimately desirable to prove them correct also, but there is
an important distinction between them and the program specifically
intended to verify the conjecture in that the latter is subject to
wishful thinking by the author and even by the referees.

	My suggestion then is that the committee offer a prize for
the first computer-checked proof (whether generated by computer or
not) that a program is correct that is the basis of a substantial
published proof of a matematical conjecture.

	There is a lesser example than the four color theorem
which I understand better.  A Stanford CS graduate student named
Oren Patashnik, while at Yale, proved that 3 dimensional tic-tac-toe
with four on a side is a win for the first player using about
1500 hours of computer time.  The paper about it was recently
published in %2Mathematics Magazine%1.  In my opinion, it wouldn't
be very hard to prove correct a program that verifies
cases.
.next page;
        Like the four color problem, Patashniks proof involved
finding winning moves in certain situations with the help of the
computer and then using the computer to verify that the moves were
winning and the positions formed an adequate set.
I think he or someone else would deserve a moderate prize for
a computer checked proof.  More than likely, a new program would
be written for the verification work that would be easier to
prove correct and would run in a reasonable time.

.reg